k:Knd, f, g:Top. (islocal(k))  (kindcase(k; a.f(a); l,t.g(l,t) ) ~ f(act(k))) 

latex

Definitions	x:A. B(x), P  Q, b, islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), act(k), b, isl(x), if b then t else f fi , lnk(k), tag(k), outr(x), tt, ff, t.1, outl(x), t.2, t  T, Knd, False, rcv(l,tg),
Lemmas	false wf, top wf, true wf, Knd wf